Em semântica formal, semântica de valor-verdade é uma alternativa à semântica tarskiana. Ela tem sido defendida principalmente por Ruth Barcan Marcus, H. Leblanc, e M. Dunn e N. Belnap. Também é chamada de interpretação substituição (dos quantificadores) ou quantificação de substituição.

A idéia dessa semântica é que o quantificador universal (existencial) pode ser lido como uma conjunção (disjunção) de fórmulas em que as constantes substituem as variáveis no escopo do quantificador. Por Exemplo. ∀xPx pode ser lido (Pa & Pb & Pc & ...) onde a, b, c são constantes individuais que substituem todas as ocorrências de x em Px.

A principal diferença entre a semântica de valor-verdade e a semântica padrão para a lógica de predicados é que não existem domínios para semântica de valor-verdade. Apenas as cláusulas verdadeiramente atômicas e as fórmulas quantificadoras diferem daquelas da semântica padrão. Considerando que, as fórmulas atômicas da semântica padrão como Pb ou RCA são verdadeiras se, e somente se, (o referente) b é um membro da extensão do predicado P, respectivamente, se e somente se o par (c, a) é um membro da extensão de R, na semântica de valor-verdade os valores-verdade de fórmulas atômicas são básicos. A fórmula universal (existencial) é verdadeira se e somente se em todos (alguns) casos de suas substituiçoes são verdadeiras. Compare isso com a semântica padrão, que diz que a fórmula universal (existencial) é verdadeira se, e somente se, para todos (alguns) membros do domínio, a fórmula valer para todos eles (alguns); por exemplo. ∀xA é verdadeira (sob uma interpretação) se e somente se para todos os k no domínio D, A (k / x) é verdadeira (em que A (k / x) é o resultado da substituição por k para todas as ocorrências de x em A ). (Aqui estamos supondo que as constantes são nomes para si mesmos, ou seja, eles também são membros do domínio.)

Semântica de valor-verdade não é livre de problemas. Primeiro, o teorema forte da completude e o teorema da compacidade falham. Para ver isto considere o conjunto {F (1), F (2), ...}. É evidente que a fórmula ∀xF (x) é uma consequência lógica do conjunto, mas não é uma consequência de qualquer subconjunto finito dela (e, portanto, não é dedutível a partir dele). Segue-se imediatamente que tanto compacidade como o teorema de completude forte falham para a semântica de valor-verdade. Este problema é retificado por uma modificação da definição de consequência lógica tal como consta em Dunn and Belnap 1968.

Outro problema ocorre na lógica livre. Considere uma linguagem com uma constante c individual que não é designada e um predicado F permanente para 'não existe'. Então ∃xFx é falsa, mesmo que uma instância de substituição (na verdade cada um desses casos sob essa interpretação) seja verdadeira. Para resolver este problema nós simplesmente adicionamos a ressalva de que uma declaração existencialmente quantificada é verdade sob uma interpretação para pelo menos um caso em que a substituição constante designa algo que existe.